This invention is related to determining if conflicting signals exist in a Boolean algorithm that represents a group of signals. More specifically, the invention is a method and apparatus for performing Boolean satisfiability testing on a Boolean algorithm using an apparatus that incorporates reconfigurable hardware in a pipelined architecture. The clauses of the Boolean algorithm are input into the reconfigurable hardware and implication and conflict analysis is performed of the variables constituting the Boolean algorithm. The invention also performs non-chronological backtracking on the variables if conflicts are uncovered. The invention is embodied in various methods, apparatuses, a hardware architecture, a computer system, and a computer program product that performs satisfiability testing on a Boolean algorithm.
The following references provide useful background information on the indicated topics, all of which relate to the invention, and are incorporated herein by reference.
Challenge Benchmarks:
DIMACS, DIMACS Challenge Benchmarks and UCSC Benchmarks, available at ftp://dimacs.rutgers.edu/pub/challenge/sat/benchmarks/cnf.
Use of reconfigurable hardware for satisfiability testing:
M. Abramovici and D. Saab, Satisfiability on Reconfigurable Hardware, Seventh International Workshop on Field Programmable Logic and Applications (1997).
Systolic processing systems:
J. Arnold, D. Buell and E. Davis, Splash 2 (Attached Processor Board), Fourth Annual ACM Symposium on Parallel Algorithms and Architectures, pp. 316-322 (1992).
Virtual wiring between FPGAs:
J. Baab, R. Tessier and A. Agarwal, Overcoming Pin Limitations In FPGA-Based Logic Emulators, IEEE Workshop on FPGA-based Custom Computing Machines, pp. 142-151 (1993).
Combinational verification for equivalence checking:
J. Burch and V. Singhal, Tight Integration Of Combinational Verification Methods, Proceedings of ICCAD, pp. 570-576 (1998).
Test generation algorithm using transitive closure computation and decision making:
S. Chakradhar, V. Agrawal and S. Rothweiler, A Transitive Closure Algorithm For Test Generation, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 12, No. 7, pp. 1015-28 (July 1993).
Uniform proof procedure for quantification theory:
M. Davis and H. Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM, Vol. 7, pp. 201-215 (1960).
Path-Oriented Decision Making (PODEM) for combinational logic circuits:
P. Goel, An Implicit Enumeration Algorithm To Generate Tests For Combinational Logic Circuits, IEEE Transactions on Computers, Vol. C30, No. 3, pp. 337-343 (March 1981).
Reduction of problem size and backtrack requirements using binary decision diagrams coupled with a Boolean satisfiability checker:
A. Gupta and P. Ashar, Integrating A Boolean Satisfiability Checker And BDDs For Combinational Verification, Proceedings of VLSI Design 98, pp. 222-225 (1998).
Using the Boolean satisfiability method for generating test patterns for single stack-at faults in combinational circuits:
T. Larrabee, Test Pattern Generation Using Boolean Satisfiability, IEEE Transactions on Computer-Aided Design, Vol. 11, No. 1, pp. 4-15, (January 1992).
Augmentation of basic backtracking with conflict analysis:
J. Silva and K. Sakallah, GRASP-A New Search Algorithm For Satisfiability, Proceedings of ICCAD, pp. 220-227 (1996).
Using reduction to satisfiability for combinational logic test generation:
P. Stephan, R. Brayton and A. Sangiovanni-Vincentelli, Combinational Test Generation Using Satisfiability, IEEE Transactions on Integrated Circuits and Systems, Vol. 15, No. 9, pp. 1167-76 (September 1996).
Solving satisfiability problems using a specialized circuit to solve each problem instance on a FPGA:
T. Suyama, M. Yokoo and H. Sawada, Solving Satisfiability Problems on FPGAs, Sixth International Workshop on Field Programmable Logic and Applications (1996).
There will now be provided a discussion of various topics to provide a proper foundation for understanding the invention.
As illustrated by the literature, Boolean Satisfiability Checking (SAT) is at the core of many applications in computer-aided design (CAD) of very large scale integrated (VLSI) circuits. A number of techniques for accelerating SAT using FPGA-based (Field Programmable Gate Arrays) instance-specific reconfigurable hardware have been proposed in the literature. While significant speedups have been reported over software implementations of SAT for a number of examples, fundamental hurdles remain before this technology can be applied widely.
The first fundamental hurdle is the time overhead for compiling the hardware implementation of the algorithm on to FPGAs. This includes the times for mapping the logic netlist onto the Combinational Logic Blocks (CLB) of the FPGA and the time for place-and-route. In most cases, this combined time can actually be comparable to or greater than the time to actually solve the formula, even in software.
The second fundamental hurdle is that the level of sophistication in the hardware algorithm is not equal to the level of the best software algorithm. The hardware algorithm basically relies on raw parallelism to achieve the speedup. As a result, it is possible to find a number of examples for which the software implementation is faster or comparable because the software heuristics work very well. In previous hardware acceleration efforts for SAT, non-chronological backtracking has been incorporated into the hardware SAT algorithm. Another major feature that often speeds up the SAT solver considerably is the addition of clauses corresponding to solution subspaces that do not need to be explored. This feature is practically impossible to implement in previous architectures.
Another fundamental drawback is that previous architectures have led to much slower clock speeds than what is potentially achievable in FPGAs. The slow clock speeds are a result of the hardwired implementation of connections between literals leading to irregular layout, long wires and wires crossing FPGA boundaries.
The Boolean satisfiability problem is a well-known constraint satisfaction problem with many applications in computer-aided design, such as test generation, logic verification and timing analysis. Given a Boolean formula, the objective is either to find an assignment of 0-1 values to the variables so that the formula evaluates to true, or to establish that such an assignment does not exist.
The Boolean formula is typically expressed in conjunctive normal form (CNF), also called product-of-sums form. Each sum term (clause) in the CNF is a sum of single literals, where a literal is a variable or its negation. An n-clause is a clause with n literals. For example, vi+vxe2x80x2j+vk is referred to as a 3-clause. In order for the entire formula to evaluate to 1, each clause must be satisfied, i.e., evaluate to 1.
Most current SAT solvers are based on the Davis-Putnam algorithm. Referring to FIG. 1, pseudo code for the basic Davis-Putnam algorithm is shown. Referring to FIG. 2, the process flow for the basic Davis-Putnam algorithm is illustrated.
The basic algorithm begins from an empty partial assignment, as shown in Step S100. At Step S110, the algorithm determines if there are any free variables available. The algorithm proceeds by assigning a 0 or 1 value to one free variable at a time. After each assignment, at Step S120, the algorithm determines the direct and transitive implications of that assignment on other variables. In Step S130, the algorithm checks contradictions. At Step S140, if no contradictions are detected during the implication procedure, the algorithm picks the next free variable at Step S150, and repeats the procedure. Otherwise, the algorithm attempts a new partial assignment by complementing the most recently assigned variable for which only one value has been tried so far, as shown in Steps S160-S180. This step is called backtracking. The algorithm terminates when no free variables are available and no contradictions have been encountered (implying that all the clauses have been satisfied and a solution has been found), or when all possible assignments have been exhausted. The algorithm is complete in that it will find a solution if it exists.
Determining implications is crucial to pruning the search space since (1) it allows the algorithm to skip entire regions of the search space corresponding to contradictory partial assignments, and (2) every implied variable corresponds to one less free variable on which search must be performed. Unfortunately, detecting implications in software is very slow since each clause containing the newly assigned or implied variable is scanned and updated sequentially, with the process repeated until no new implications are detected.
The potential for hardware speedup potential in the SAT algorithm stems from recognizing that the implication procedure central to the algorithm is both highly parallelizable and easily mapped to basic logic gates.
Recent literature in the field discusses software implementations of the Davis-Putnam algorithm that have enhanced the algorithm in various ways while maintaining the same basic flow. The contribution of the GRASP work is notable since it applies non-chronological backtracking (conflict analysis) and dynamic clause addition to prune the search space further.
Conflict analysis and clause addition are relative easy to implement in software. When a new value is implied, it is added to a data structure recording the implication graph. When a conflict occurs, traversing the graph backwards identifies predecessors of the conflict. It is also easy to add new clauses to the clause database. Such techniques may greatly improve the performance on many problems.
Much of the performance improvement reported by GRASP comes from its implementation of conflict analysis. When the basic Davis-Putnam algorithm observes a conflict, it backtracks to change the partial assignment. It does not, however, analyze which variable is the true reason for the observed conflict. The backtracking process may complement variables irrelevant to the conflict and repeatedly explore related dead ends. More sophisticated conflict analysis works to identify the variable assignments that lead to the conflict. Acting as a reverse implication procedure, conflict analysis identifies the transitive predecessors of the implied literals leading to the conflict.
Consider, for example, the Boolean formula composed of the following 3-clauses in Equation (1):
xe2x80x83(v1xe2x80x2+v8+v9)(v2xe2x80x2+v8+v9xe2x80x2) (vxe2x80x21+v8xe2x80x2+v10) (v3xe2x80x2+v8xe2x80x2+v10xe2x80x2)xe2x80x83xe2x80x83Equation (1)
If v1, v2 . . . v7 are previously assigned to 1 and then v8 is assigned to 1, the resulting implication graph is shown in FIG. 3A. A conflict is detected on v10. The predecessors for the conflict are v1, v3 and v8. Similarly, when v8 is changed to 0 (see FIG. 3B), it generates a conflict in v9. The causes of the conflict are v1, v2 and v8xe2x80x2. At this point, we know that either value of v8 will lead to a conflict. The basic algorithm would change the value of v7 to 0 and try again. However, v1, v2 and v3 are actually responsible for the conflicts. Therefore, we can directly backtrack to the most recently assigned variable causing the dual conflict, i.e., v3. This is called non-chronological backtrack.
In general, when we first meet a conflict on branch variable vk, we can identify the predecessor set as P(vk). Then if we have a conflict for vkxe2x80x2, we can get another predecessor set P(vkxe2x80x2). The union of the two sets, excluding vk and vkxe2x80x2, is the predecessor that leads to the double conflict in vk. We can backtrack to the variables in this set.
In the previous example, conflict analysis reveals that if v1, V2 and v3 are all 1, the formula can not be satisfied. This is a hidden constraint not directly manifested as a clause. We can add a new clause (v1xe2x80x2+v2xe2x80x2+v3xe2x80x2) to the Boolean formula being solved. Adding this clause to the formula allows the solver to detect this conflict earlier and avoid exploring the same space in the future search.
Conflict analysis and clause addition are relative easy to implement in software. When a new value is implied, it is added to a data structure recording the implication graph. When a conflict occurs, traversing the implication graph backwards identifies predecessors of the conflict. It is also easy to add new clauses to the clause database. Such techniques may greatly improve the performance on many problems.
The literature includes several proposals for solving SAT using reconfigurable hardware. Suyama, et al. propose their own SAT algorithm distinct from the Davis-Putnam approach. Their approach is characterized by the fact that at any point, a full (not partial) variable assignment is evaluated. While Suyama, et al. propose heuristics to prune the search space, they acknowledge that the number of states visited in their approach can be up to eight times the number of states visited in the basic Davis-Putnam approach.
The work by Abramovici and Saab also proposed a configurable hardware SAT solver. Their approach basically amounts to an implementation of a PODEM-based (Path-Oriented DEcision Making) algorithm in reconfigurable hardware. PODEM is typically used to solve test generation problems. Unlike PODEM, which relies on controlling and observing the primary inputs and outputs of a circuit, the Davis-Putnam algorithm also captures relationships between the internal variables in the circuit; this significantly reduces the state space visited and the run time.
In addition, previous hardware SAT solvers described in the literature do not employ dynamic clause addition. Importantly, all the previous approaches generate formula-specific solver circuits that differ significantly from formula to formula. As a result, the entire circuit for each formula must be completely synthesized, placed and routed and downloaded to the multiple FPGAs from scratchxe2x80x94a significant run time overhead.
The invention has been made in view of the above circumstances and has an object to overcome the above problems and limitations of the prior art, and has a further object to provide the capability to for solving Boolean SAT formulas.
Additional objects and advantages of the invention will be set forth in part in the description that follows and in part will be obvious from the description, or may be learned by practice of the invention. The objects and advantages of the invention may be realized and attained by means of the instrumentalities and combinations particularly pointed out in the appended claims.
It is a further object of the invention to provide a method, a computer system and a computer program product for solving a Boolean SAT formula.
It is yet a further object of the invention to provide a method, a computer system and a computer program product for creating a Boolean SAT solver for solving a Boolean SAT formula.
It is still a further object of the invention to provide a method and an apparatus for downloading and partitioning a Boolean SAT formula and loading the partitions into processing elements for solving the SAT formula.
The above and other objects of the invention are accomplished by providing an apparatus the uses a ring topology pipeline bus between the processing elements and the control device to pass variables from a Boolean SAT formula for processing.
The above and further objects of the invention are further accomplished by providing a method and an apparatus that dynamically adds redundant clauses to a Boolean SAT formula to uncover hidden constraints.
The above objects are further achieved by providing a method for computing implications and conflicts between the variables in a Boolean SAT formula and executing non-chronological backtracking to resolve the conflicts that are found.
Preferably, the above objects are achieved by providing a method of creating a Boolean SAT solver apparatus for solving a Boolean SAT formula, wherein the Boolean SAT solver includes a plurality of reconfigurable hardware modules, the method including reading the Boolean SAT formula, partitioning the Boolean SAT formula and limiting each partition to a predetermined number of variables, configuring the plurality of reconfigurable modules to form circuit arrays, assigning the partitions of the Boolean SAT formula to the circuit arrays in each of the plurality of reconfigurable hardware modules, and programming the functions and connections specific to each partition of the Boolean SAT formula within each of the plurality of reconfigurable hardware modules.
Preferably, the above objects are further achieved by providing a method for solving a Boolean SAT formula containing a plurality of Boolean variables using a Boolean SAT solver comprised of a plurality of reconfigurable hardware modules, the method including the steps of setting the plurality of Boolean variables to a known state, selecting a free variable from the plurality of Boolean variables and assigning a known value to the selected free variable or indicating that all the variables have been assigned and the Boolean SAT formula solved, dependent upon the outcome of selecting a free variable, assigning a predetermined value to the free variable, computing the logical implication of the assignment to the free variable and either performing conflict analysis on the free variable or selecting another free variable from the plurality of Boolean variables dependent upon the outcome of the logical implication, performing conflict analysis on any conflicts that arise from the logical implication of the free variable, and determining whether to backtrack through the predecessor variables that obtained their value from the assigned free variable and backtracking through the predecessor variables and restarting the logical implication or indicating that the Boolean SAT formula is unsolvable, dependent upon the outcome of the backtrack determination.
Preferably, the above objects are further achieved by providing a computer system adapted to solving a Boolean SAT formula containing a plurality of Boolean variables, including a processor and a memory including software instructions adapted to enable the computer system to perform the steps of setting the plurality of Boolean variables to a known state, selecting a free variable from the plurality of Boolean variables and assigning a known value to the selected free variable or indicating that all the variables have been assigned and the Boolean SAT formula solved, dependent upon the outcome of selecting a free variable, assigning a predetermined value to the free variable, computing the logical implication of the assignment to the free variable and either performing conflict analysis on the free variable or selecting another free variable from the plurality of Boolean variables dependent upon the outcome of the logical implication, performing conflict analysis on any conflicts that arise from the logical implication of the free variable, and determining whether to backtrack through the predecessor variables that obtained their value from the assigned free variable and backtracking through the predecessor variables and restarting the logical implication or indicating that the Boolean SAT formula is unsolvable, dependent upon the outcome of the backtrack determination.
Preferably, the above objects are further achieved by providing a computer program product for enabling a computer to solve a Boolean SAT formula containing a plurality of Boolean variables, the computer program product including software instructions for enabling the computer to perform predetermined operations, and a computer readable medium bearing the software instructions, the predetermined operations including the steps of setting the plurality of Boolean variables to a known state, selecting a free variable from the plurality of Boolean variables and assigning a known value to the selected free variable or indicating that all the variables have been assigned and the Boolean SAT formula solved, dependent upon the outcome of selecting a free variable, assigning a predetermined value to the free variable, computing the logical implication of the assignment to the free variable and either performing conflict analysis on the free variable or selecting another free variable from the plurality of Boolean variables dependent upon the outcome of the logical implication, performing conflict analysis on any conflicts that arise from the logical implication of the free variable, and determining whether to backtrack through the predecessor variables that obtained their value from the assigned free variable and backtracking through the predecessor variables and restarting the logical implication or indicating that the Boolean SAT formula is unsolvable, dependent upon the outcome of the backtrack determination.
Preferably, the above objects are further achieved by providing a method of solving a Boolean SAT formula containing a plurality of Boolean variables using a solver apparatus, wherein the solver apparatus includes a plurality of processing elements, a control device, a pipeline bus interconnecting the plurality of processing elements and the control device in a ring, and a host computer interconnected to the control device, the method including downloading the Boolean SAT formula to the control device, partitioning the Boolean SAT formula and loading the portions into the plurality of processing elements, initializing the plurality of variables of the Boolean SAT formula to a known value, attempting to select a free variable from the plurality of Boolean variables and either assigning the free variable a known value or indicating that the Boolean SAT formula is solved, dependent upon the attempt to assign a known value to a free variable, computing the logical implication of the assignment to the free variable and either performing conflict analysis on the free variable or selecting another free variable from the plurality of Boolean variables for assignment, dependent upon the outcome of the logical implication, performing conflict analysis on any conflicts that arise from the logical implication of the free variable, and determining whether to backtrack through the predecessor variables that obtained their value from the assigned free variable and backtracking through the predecessor variables and restarting the logical implication or indicating that the Boolean SAT formula is unsolvable, dependent upon the outcome of the backtrack determination.
Preferably, the above objects are further achieved by providing an apparatus for downloading a Boolean SAT solver algorithm and formula, and solving the corresponding Boolean SAT problem, the architecture comprising at least one clause module for implementing the Boolean SAT solver algorithm, a control device for receiving the Boolean SAT solver algorithm and formula and distributing the Boolean SAT solver algorithm and formula to the at least one clause module, a pipeline bus interconnecting the control device and the at least one clause module in a ring topology, thereby allowing the Boolean SAT solver algorithm, formula and variable values to be passed between the control device and the at least one clause module, and between clause modules, and a host computer for downloading the Boolean SAT solver algorithm and formula to the control device and receiving results therefrom.